COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	VAR: x,y,z
C00003 ENDMK
C⊗;
VAR: x,y,z;
INF_PRED:=; EQUALITY:=;
INF_OP:⊗;
PRE_OP:g,e;

g1:(x⊗y)⊗z=x⊗(y⊗z);
g2:e⊗x=x;
g3:g(x)⊗x=e;
THM:x⊗e=x; ;